{-
 -  Separ, Type/Normalize.hs
 -
 -  Copyright (c) 2010 Dariusz Leniowski. All Rights Reserved.
 -
 -  Redistribution and use in source and binary forms, with or without 
 -  modification, are permitted provided that the following conditions 
 -  are met:
 -
 -  1. Redistributions of source code must retain the above copyright 
 -     notice, this list of conditions and the following disclaimer.
 -
 -  2. Redistributions in binary form must reproduce the above copyright 
 -     notice, this list of conditions and the following disclaimer 
 -     in the documentation and/or other materials provided with 
 -     the distribution.
 -
 -  3. The name of the author may not be used to endorse or promote 
 -     products derived from this software without specific prior 
 -     written permission.
 -
 -  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 
 -  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 
 -  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS 
 -  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL 
 -  THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, 
 -  INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES 
 -  (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS 
 -  OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) 
 -  HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, 
 -  STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING 
 -  IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 
 -  POSSIBILITY OF SUCH DAMAGE.
 -
 -}

{-# LANGUAGE ExistentialQuantification, RankNTypes, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, TypeSynonymInstances, RelaxedPolyRec #-} 

module Type.Normalize where

import Data.Set as Set
import Data.Map as Map
import qualified Data.IntSet as RefSet

import Type.Base hiding (value)

type RefSet = RefSet.IntSet

-----------------------------------------------
-- NORMALIZATION
-----------------------------------------------
--
-- class Normalizable a where
--     normalize :: forall b. a -> MM b -> MM (a,b)
-- 
-- normalize object continuation ~> MM (object',contResult)
--
-- normalization has three parts
-- 1. open all quantifiers (unquantify) and gather equations (eqs and leqs)
--    so all variables will reside in context to be ready to be bound
-- 2. do something (what to do is expressed in continuation) with all the
--    variables and formulae (i.e. optimize bounds, graphCCC and so on)
-- 3. close all quantifiers (quantify) in correct order and ensure
--    formulae where needed (i.e. when they do not depend on any variables)
--
-- Types are normalized to be in order Var Lam PSet Lca Gcd Ref Cls, 
--     App and PGet are handled separately
-- Formulae are normalized to rid of TTs and nested Ands [[[]]] and
--     stores all Eqs and Leqs in context to be normalized in 2nd phase
-- FInfo normalizes formulae related to vars in FInfo in question
--


-- some utility function
pair :: Monad m => a -> b -> m (a,b)
pair a b = return (a,b)

instance Normalizable NormalizableType where
	normalize (N a) k = do
		(a',k') <- normalize a k
		return (N a',k')
instance Normalizable () where
	normalize () k = k >>= (pair ())
instance (Normalizable a, Normalizable b) => Normalizable (a,b) where
	normalize (a,b) k = do
		(a',(b',w)) <- normalize a $ normalize b k
		return ((a',b'),w)
instance Normalizable a => Normalizable [a] where
	normalize [] k = k >>= (pair [])
	normalize (x:xs) k = do
		(x',(xs',w)) <- normalize x (normalize xs k)
		return (x':xs',w)
instance (Ord a,Normalizable a) => Normalizable (Set a) where
	normalize s k0 = Set.fold f (k0 >>= pair Set.empty) s where
		f elm k = do
			(elm',(set,w)) <- normalize elm k
			return (Set.insert elm' set,w)
instance (Ord key, Normalizable a) => Normalizable (Map key a) where
	normalize m k0 = Map.foldrWithKey f (k0 >>= pair Map.empty) m where
		f key elm k = do
			(elm',(mp,w)) <- normalize elm k
			return (Map.insert key elm' mp,w)

-- normalize type to order Var Lam PSet Lca Gcd Ref Cls
instance (Lambdable Type, Quantifiable Type, Quantifiable Formulae, UniLoop ()) => Normalizable Type where
	normalize t@(Cls _) k = k >>= (pair t)
	normalize t@(Ref r) k = do
		free <- isVarFree r
		if free then k >>= (pair t) else do
			value <- getVarValue r
			normalize value k
	normalize   (Gcd a@(Var _ _ _ _) b) k = do
		(a',i) <- unquantify False a
		(i',(v,w)) <- normalize i $ normalize (Gcd a' b) k
		v' <- quantify i' v
		return (v',w)
	normalize   (Gcd a b@(Var _ _ _ _)) k = normalize (Gcd b a) k
	normalize   (Gcd (Lam b a1 r1) c) k = do
		-- Lam is contravariant in 'argument' argument
		(a2,r2,vs) <- makeLam False b c
		(vs',(a,(r,w))) <- 
			-- therefore Lca here
			normalize vs $ normalize (Lca a1 a2) $ normalize (Gcd r1 r2) k
		t' <- quantify vs' (Lam b a r)
		return (t',w)
	normalize   (Gcd a b@(Lam _ _ _)) k = normalize (Gcd b a) k
	normalize   (Gcd (Lca a b) c) k = do
		-- I assume that my lattice is distributive i.e.
		-- (a `lca` b) `gcd` c = (a `gcd` c) `lca` (b `gcd` c)
		-- which is (in case of lattices) equivalent to
		-- (a `gcd` b) `lca` c = (a `lca` c) `gcd` (b `lca` c)
		(aa,(bb,w)) <- normalize (Gcd a c) $ normalize (Gcd b c) k
		return (Lca aa bb,w)
	normalize   (Gcd a (Lca b c)) k = do
		-- same as above
		(aa,(bb,w)) <- normalize (Gcd a b) $ normalize (Gcd a c) k
		return (Lca aa bb,w)
	normalize   (Gcd a b) k = do
		(a',(b',w)) <- normalize a $ normalize b k
		return (Gcd a' b',w)
	normalize   (Lca a@(Var _ _ _ _) b) k = do
		(a',i) <- unquantify False a
		(i',(v,w)) <- normalize i $ normalize (Lca a' b) k
		v' <- quantify i' v
		return (v',w)
	normalize   (Lca a b@(Var _ _ _ _)) k = normalize (Lca b a) k
	normalize   (Lca (Lam b a1 r1) c) k = do
		-- Lam is contravariant in 'argument' argument
		(a2,r2,vs) <- makeLam False b c
		(vs',(a,(r,w))) <- 
			normalize vs $ normalize (Gcd a1 a2) $ normalize (Lca r1 r2) k
		v <- quantify vs' (Lam b a r)
		return (v,w)
	normalize   (Lca a b@(Lam _ _ _)) k = normalize (Lca b a) k
	normalize   (Lca a b) k = do
		(a',(b',w)) <- normalize a $ normalize b k
		return (Lca a' b', w)
	normalize   (Lam b a r) k = do
		(a',(r',w)) <- normalize a $ normalize r k
		return (Lam b a' r',w)
	normalize t@(Var _ _ _ _) k = do
		(u,i) <- unquantify False t
		(i',(u',w)) <- normalize i $ normalize u k
		v <- quantify i' u'
		return (v,w)
	normalize   (App b f x) k = do
		(f',(x',w)) <- normalize f $ normalize x k
		return (App b f' x',w)
	normalize   (PSet (Lam b a r) n v) k = 
		normalize (Lam b a (pSet r n v)) k
	normalize   (PSet (Var x b f t) n v) k = 
		normalize (Var x b f (pSet t n v)) k
	normalize t@(PSet _ _ _) k = do
		-- gather all properties into one map so doubles
		-- will be ridden of and normalize it all in one run
		let (u,m) = gather t Map.empty
		(u',(m',w)) <- normalize u $ normalize m k
		let t' = Map.foldrWithKey (\n v r -> pSet r n v) u' m'
		return (t',w)
		where 
			gather (PSet e n v) a = 
				-- from two props get the old one
				gather e $ Map.insertWith (\_ o -> o) n v a
			gather e a = (e,a)
	normalize   (PGet t n) k = do
		(t',w) <- normalize t k
		return (PGet t' n,w)

-- normalize formulae, there's no real order here, 
--     filter Ands from TT's, normalize types in Eqs and Leqs
-- eqs and leqs are stored in context and they will be taken care of
-- after the first phase of normalization, besides that,
-- nothing happens here
instance (Quantifiable Formulae, UniLoop ()) => Normalizable Formulae where
	normalize TT k = k >>= (pair TT)
	normalize FF k = k >>= (pair FF)
	normalize (And ls) k = do
		(ls',w) <- normalize ls k
		return (normAnd ls' [],w) where
			normAnd [] [ ] = TT
			normAnd [] [f] = f
			normAnd []  a  = (And a)
			normAnd (TT:xs) a = normAnd xs a
			normAnd (FF: _) _ = FF
			normAnd ((And as):xs) a = rs $ normAnd as a where
				rs TT = normAnd xs []
				rs FF = FF
				rs (And b) = normAnd xs b
				rs f = normAnd xs [f]
			normAnd (x:xs) a = normAnd xs (x:a)
	normalize (Eq a b) k = do
		i <- pushEq (Eq a b)
		w <- k
		e <- popEq i
		return (e,w)
	normalize (Leq e a b) k = do
		i <- pushEq (Leq e a b)
		w <- k
		l <- popEq i
		return (l,w)
	normalize f@(Qua q _ _ _ _) k = do
		(f',i) <- unquantify q f 
		(i',(f'',w)) <- normalize i $ normalize f' k
		f''' <- quantify i' f''
		return (f''',w)
	
-- normalize FInfo (normalize formulae from unquantified variables)
-- this is strange one, because there's nothing to normalize
-- in list of (Bool,RefType), still there are formulae from
-- quantifiers both Var and Qua and here those formulae are
-- being taken care of
-- 
-- when var was instantiated, it is nothing special, just another
-- formulae, because 
--     \exists x \in P(x) . Q(x) 
-- means just 
--     \exists x \in \Omega . P(x) and Q(x)
--
-- on the other hand, when var was skolemized, special care should be
-- taken because
--     1. (Eq skolem = Class) would fail, 
--     2. On properties ensured by the formulae later 
--        computation may depend,
--     3. There is no shortcut for \forall x \in P(x) . Q(x) 
--        (we have no `==>' operator)
-- therefore when var was skolemized, it is first marked as instantiated
-- then related formulae are normalized and after that the var is marked
-- as skolem again
--
-- this approach may be flawed, still it is the best 
-- I could come up with for now, sorry ;-)
--
instance (Quantifiable Formulae, UniLoop ()) => Normalizable FInfo where
	normalize (FInfo []) k = k >>= (pair (FInfo []))
	normalize (FInfo ((False,r):rs)) k = do 
		f <- getVarFormulae r
		setVarFormulae r TT
		(f',(FInfo rs',w)) <- normalize f $ normalize (FInfo rs) k
		getVarFormulae r >>= (setVarFormulae r . fand f')
		return (FInfo ((False,r):rs'),w)
	normalize (FInfo ((True,r):rs)) k = do 
		f <- getVarFormulae r
		setVarFormulae r TT
		makeVarInst r
		pushEqMap
		(f',(FInfo rs',w)) <- normalize f $ 
			do uniLoopK (return ()); popEqMap; makeVarSkolem r; normalize (FInfo rs) k
		getVarFormulae r >>= (setVarFormulae r . fand f')
		return (FInfo ((True,r):rs'),w)

